symmetrize_com 12,41
The 'Type' type for T was necessary for
proving the lemma eqvtype_wf in theory
subtyping. With 'Type', the type of symmetrize
was unnecessarily tied to the type
of the arguments a and b.

origin